This paper starts by investigating Ackermann's interpretation of finite set theory in the natural numbers. We give a formal version of this interpretation from Peano arithmetic (PA) to Zermelo-Fraenkel set theory with the infinity axiom negated (ZF−inf) and provide an inverse interpretation going the other way. In particular, we emphasize the precise axiomatization of our set theory that is required and point out the necessity of the axiom of transitive containment or (equivalently) the axiom scheme of ∈-induction. This clarifies the (...) nature of the equivalence of PA and ZF−inf and corrects some errors in the literature. We also survey the restrictions of the Ackermann interpretation and its inverse to subsystems of PA and ZF−inf, where full induction, replacement, or separation is not assumed. The paper concludes with a discussion on the problems one faces when the totality of exponentiation fails, or when the existence of unordered pairs or power sets is not guaranteed. (shrink)

The foundation scheme in set theory asserts that every nonempty class has an ∈\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\in $$\end{document}-minimal element. In this paper, we investigate the logical strength of the foundation principle in basic set theory and α\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\alpha $$\end{document}-recursion theory. We take KP set theory without foundation as the base theory. We show that KP-\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^-$$\end{document} + Π1\documentclass[12pt]{minimal} \usepackage{amsmath} (...) \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\Pi _1$$\end{document}-Foundation + V=L\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$V=L$$\end{document} is enough to carry out finite injury arguments in α\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\alpha $$\end{document}-recursion theory, proving both the Friedberg-Muchnik theorem and the Sacks splitting theorem in this theory. In addition, we compare the strengths of some fragments of KP. (shrink)

In an earlier paper the first author initiated the study of generic cuts of a model of Peano arithmetic relative to a notion of an indicator in the model. This paper extends that work. We generalise the idea of an indicator to a related neighbourhood system; this allows the theory to be extended to one that includes the case of elementary cuts. Most results transfer to this more general context, and in particular we obtain the idea of a generic cut (...) relative to a neighbourhood system, which is studied in more detail. The main new result on generic cuts presented here is a description of truth in the structure , where I is a generic cut of a model M of Peano arithmetic. The special case of elementary generic cuts provides a partial answer to a question of Kossak [R. Kossak, Four problems concerning recursively saturated models of arithmetic, Notre Dame Journal of Formal Logic 36 519–530]. (shrink)

We prove that any proof of a [Formula: see text] sentence in the theory [Formula: see text] can be translated into a proof in [Formula: see text] at the cost of a polynomial increase in size. In fact, the proof in [Formula: see text] can be obtained by a polynomial-time algorithm. On the other hand, [Formula: see text] has nonelementary speedup over the weaker base theory [Formula: see text] for proofs of [Formula: see text] sentences. We also show that for (...) [Formula: see text], proofs of [Formula: see text] sentences in [Formula: see text] can be translated into proofs in [Formula: see text] at a polynomial cost in size. Moreover, the [Formula: see text]-conservativity of [Formula: see text] over [Formula: see text] can be proved in [Formula: see text], a fragment of bounded arithmetic corresponding to polynomial-time computation. For [Formula: see text], this answers a question of Clote, Hájek and Paris. (shrink)

This paper introduces a new theory of constant regions, which generalizes that of interstices, in nonstandard models of arithmetic. In particular, we show that two homogeneity notions introduced by Richard Kaye and the author, namely, constantness and pregenericity, are equivalent. This led to some new characterizations of generic cuts in terms of existential closedness.